x, tg:Id, k:Knd, l:IdLnk, T, A, B:Type, f:(AB(T List)).
(rcv(l,tg) = k  T = B)
 @source(l): k(v) sends [tg,   f(x, v)] on link l    Dsys
 & (D:Dsys.
 & (@source(l): k(v) sends [tg,   f(x, v)] on link l    D
 & ( D 
 & ( realizes es.
 & ( vartype(source(l);x)  A
 & ( & (e:E. loc(e) = source(l)  Id  kind(e) = k  Knd  valtype(e)  B)
 & ( & (e:E. kind(e) = rcv(l,tg)  Knd  valtype(e)  T)
 & ( & (e:E.
 & ( & (loc(e) = source(l)  Id
 & ( & ( kind(e) = k  Knd
 & ( & ( (L:{e':E| kind(e') = rcv(l,tg)  Knd } List.
 & ( & ( ((e':E. (e'  L)  kind(e') = rcv(l,tg)  Knd & sender(e') = e  E)
 & ( & ( (& (e1, e2:E. e1 before e2  L  (e1 <loc e2))
 & ( & ( (& map(e'.val(e');L) = f((x when e),val(e))  T List))) 

latex

Definitions

x:A. B(x), P  Q, t  T, a(v) sends [tg,   f(x, v)] on link l  , x. t(x), Prop, Top, S  T, Valtype(da;k), if b t else f fi, true, false, A & B, D realizes es. P(es), P & Q, T, True, rcv(l,tg), b, isrcv(e), isrcv(k), SQType(T), {T}, isl(x), lnk(e), lnk(k), 1of(t), outl(x), b, xL. P(x), AB, A, False, {i..j}, i  j < k, x:A. B(x), P  Q, P  Q, f o g, 2of(t), x(s), , Unit, map(f;as), tagged-list-messages(s;v;L), concat(ll), reduce(f;k;as), Y, (x  l), , State(ds), , a = b

Lemmas

s-sends-rule, lsrc wf, fpf-single wf, fpf-join wf, Knd wf, Kind-deq wf, rcv wf, IdLnk wf, Id wf, fpf-cap-single1, id-deq wf, fpf-cap wf, top wf, ma-valtype wf, fpf-join-cap-sq, fpf-dom wf, bool wf, eqtt to assert, subtype rel self, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, fpf-single-dom, possible-world wf, fair-fifo wf, world wf, d-sub wf, dsys wf, subtype rel wf, squash wf, true wf, es-valtype wf, es-kind wf, w-es wf, es-loc wf, es-E wf, Knd sq, fpf-cap-single, fpf-single-dom-sq, eq knd wf, btrue wf, assert-eq-knd, es-rcv-kind, l member wf, es-isrcv wf, es-lnk wf, es-when wf, es-vartype wf, es-val wf, append nil sq, map wf, select wf, le wf, length wf1, length-map, select-map, non neg length, pi2 wf, pi1 wf, es-tag wf, event system wf, list-set-type2, es-sender wf, es-kind-rcv, map-map, subtype rel list, map-id, member map, eqof eq btrue, Id sq